Nuprl Lemma : qoset_trans
13,42
postcript
pdf
s
:QOSet,
a
,
b
,
c
:|
s
|. (
a
b
)
(
b
c
)
(
a
c
)
latex
Up
sets
1
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
Trans(
T
;
x
,
y
.
E
(
x
;
y
))
,
Refl(
T
;
x
,
y
.
E
(
x
;
y
))
,
P
&
Q
,
Preorder(
T
;
x
,
y
.
R
(
x
;
y
))
Lemmas
qoset
wf
,
qoset
properties
origin
s:QOSet, a, b, c:|s|. (a 
b) 
(b c) (a c) s:QOSet, a, b, c:|s|. (a b) (b c) (a c) 
Tx:A. B(x)